ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  Valtype(da;kind(e)))
 (n:, e1, e2:{e:E| loc(e) = i }. Dec(ecl-es-act(es;n;x)(e1,e2))) 

latex

Definitions

x:A. B(x), P  Q, t  T, x. t(x), Top, S  T, Dec(P), P  Q, A, {T}, False, ||as||, ij, t  ...$L, Y, AB, let x,y,z = a in t(x;y;z), Prop, Valtype(da;k), ecl-trans-act(ds;da;A), x:A. B(x), P & Q, event-info(ds;da), A & B, P  Q, P  Q, x(s), b, null(as), true, false, if b t else f fi

Lemmas

decidable functionality, ecl-es-act wf, ecl-act wf, es-hist wf, ecl-es-act-ecl-act, event-info wf, es-E wf, Id wf, es-loc wf, nat wf, es-valtype wf, ma-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, ecl wf, fpf wf, Knd wf, ecl-trans-property, ecl-trans-act wf, ecl-trans wf, decidable assert, null wf3, length wf1, non neg length, length cons, length nil, length append, last lemma, last wf, decidable cand, l member wf, ecl-trans-ks wf, decidable l member, decidable equal Kind, assert wf, not wf, append wf, decl-state wf, Kind-deq wf, ecl-trans-a wf, ecl-trans-state wf, general-append-cancellation, cons one one